COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	coales[f80,jmc]		specifying a program for coalescing list structures
C00005 ENDMK
C⊗;
coales[f80,jmc]		specifying a program for coalescing list structures

	Winston and Horn, p.70, give the problem of getting the
a list of the equivalence classes of an equivalence relation given
by listing pairs of equivalent elements.  The problem is more general,
and the recursion works better, if instead of allowing merely the
a list of pairs, we allow lists of any length whose elements are all
equivalent.  If the function is to be called ⊗coalesce, then we have

coalesce ((A B) (A C) (D E F) (E G H)) = ((A B C) (D E F G H))

or some other list of lists where each sublist may have the
same elements in a different order and the sublists may be in
a different order.  In other words the answer is to be regarded as
a set of sets.  COALES.LSP[F80,JMC] is a debugged LISP program.

	What are the specifications for ⊗coalesce? 

	We have a predicate %2proper u%1 asserting that none of
the sublists of ⊗u have repeated elements, and we make assertion
about %2coalesce u%1 only for proper arguments ⊗u.  
We have

%2proper u ⊃ proper coalesce u%1

%2∀u.(proper u ⊃ ∀w1 w2.[istail[w1, coalesce u] ∧ istail[w2, coalesce u]
∧ ¬null w1 ∧ ¬null w2 ∧ w1 ≠ w2 ⊃ set qa w1 ∩ set qa w2 = <empty>]%1

This one is a pain to state, because we want to say that coalesce u
has no repeated elements and that elements don't intersect.

%2∀u. union(v ε set u, set v) = union(v ε set coalesce u, set v)%1

We also want to say that the above properties characterize %2coalesce u%1
as a list representing a set of sets, i.e. any ⊗w representing
a set of sets satisfying the above conditions will be equal to
%2coalesce_u%1 as a set of sets.